the_w:World, e:E, t, t':.
FairFifo
 isrcv(kind(e))
 match(lnk(kind(e));t;time(e))
 match(lnk(kind(e));t';time(e))
 t = t'   

latex

Definitions

time(e), kind(e), lnk(k), match(l;t;t'), b, A, P  Q, a<b, isrcv(k), FairFifo, , x:A. B(x), E, World, x:AB(x), P & Q, t  T, x:AB(x), P  Q, False, {x:A| B(x) }, Prop, Void, AB, , ij, snds(l;t), ||as||, source(l), m(i;t), onlnk(l;mss), n+m, upto(n), Type, #$n, {i..j}, S  T, i  j < k, S  T, map(f;as), concat(ll), <a,b>, w.M, mlnk(m), Id, Msg(M), m(l;t), f(a), Msg, type List, s = t, x.A(x), True, T, P  Q, as @ bs, left+right, P  Q, Dec(P)

Lemmas

decidable lt, concat map upto, iseg length, append wf, squash wf, true wf, length append, w-onlnk wf, w-m wf, Msg wf, Id wf, mlnk wf, w-M wf, lsrc wf, length wf1, concat wf, map wf, le wf, int seg wf, w-Msg wf, upto wf, isrcv wf, fair-fifo wf, nat wf, w-E wf, world wf, assert wf, w-match wf, assert-w-match, lnk wf, w-ekind wf, w-time wf